00100	GIVEAX(TRANSLE,(∀ X)(∀ Y)(∀ Z)(X<Y∧Y<Z⊃X<Z));
00200	
00300	GIVEAX(IRREF,(∀ X)(∀ Y)(X<Y⊃X≠Y));
00400	
00500	GIVEAX(LESEQ,(∀ X)(∀ Y)(X≤Y≡X<Y∨X=Y));
     

00500	END;